COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	chess[e82,jmc]		Notes on the Berliner thesis position
C00007 ENDMK
C⊗;
chess[e82,jmc]		Notes on the Berliner thesis position

must(Black,p)	To avoid loss black must ensure that  p  is true.
Here we consider that  p  is a timeless assertion.  Thus  p  contains
within it any temporality that is required.  If we ever deduce
must(Black, not p), we will know that Black loses, since he must
ensure falsity.

holds(p) ⊃ can(White,q)  We also consider that  q  contains any
temporality that may be required.

In the Berliner position,  p  will be the assertion that Black
keeps his king within the 8 squares that prevent promotion of
the white pawn.  q will be the assertion that White can reach
b5  with his king.

In this kind of argument, if we have established  must(Black,p),
we can use  p  (or  holds(p)  if it turns out that reifying is required)
as a premiss in proving  can(White,q).  It seems that we needn't
even prove  can(Black,q),  because if Black must do something
impossible, then he loses.  (This wouldn't be so in a more
general (e.g. contractual) setting, because if someone has promised
to do what may be impossible, you had better limit your bet that it
will be done to what might be collected from his in case of
default).

The key idea here is that each player has control of certain variables,
and the outcome is a function of them.  However, we are not interested
in the general situation to which the considerations of game theory
apply but in those situations in which one player can force a win.
However, we want something more abstract than the alternation of
moves, because there is an opportunity to prove things with much
less tree search.

Now how about

can(White,r)  Here  r  means an aspect of White's strategy - namely
white will push the pawn if Black moves his king out of the eight
squares.  can(White,r)  is proved by the fact that it concerns
matters entirely under the control of White.

chooses(White,r) ⊃ must(Black,p).  This is the argument that  if
White is committed to pushing the pawn if Black moves out of the eight,
then Black must stay in the eight; proving this requires the chess
argument that pushing the pawn will win if Black leaves the eight.

chooses(Black,p) ⊃ can(White,s).  This is the argument that if
Black stays within the eight, White can reach  b5.

can(White,s and r).  This is the argument that following the path
to  b5  and being ready to push if Black leaves the eight are
compatible.  The temporal relations of the commitments involved
in  s  and  r  are crucial here.

achieves(White, s and r, u).  u  is the assertion that White reaches
b5  with Black still within the eight.  This should result in

can(White, u).  Perhaps the  achieves(White, s and r, u)  can be omitted
and we can go to this last assertion directly.  Notice that the element
of coercion involved in  must(Black,p) is implicitly used here.